Normal subgroups and quotient groups #2854

Taneb · 2025-10-31T06:41:58Z

Builds off #2852, continuing towards #2729 in bitesize chunks.

jamesmckinna

This all looks great. I've made suggestions, but nothing is a deal-breaker.

src/Algebra/NormalSubgroup.agda

jamesmckinna · 2025-10-31T08:00:00Z

src/Algebra/Construct/Quotient/Group.agda

+quotientGroup : Group c (c ⊔ ℓ ⊔ c′)
+quotientGroup = record { isGroup = quotientIsGroup }
+
+project : Group.Carrier G → Group.Carrier quotientGroup


My personal preference is for π (for projection), echoing ι (for inclusion), but I won't fight for it...
... maybe I should?

I've got no strong feeling here

I noted that every time I used normal it was under sym This felt like a good reason to reverse it

src/Algebra/Construct/Quotient/Group.agda

src/Algebra/NormalSubgroup.agda

src/Algebra/Construct/Quotient/Group.agda

src/Algebra/NormalSubgroup.agda

jamesmckinna · 2025-11-04T08:42:25Z

src/Algebra/Construct/Quotient/Group.agda

+private
+  module N = NormalSubgroup N
+open NormalSubgroup N using (ι; module ι; conjugate; normal)


Can simplify this to:

Suggested change

private

module N = NormalSubgroup N

open NormalSubgroup N using (ι; module ι; conjugate; normal)

private

open module N = NormalSubgroup N using (ι; module ι; conjugate; normal)

jamesmckinna · 2025-11-04T08:47:26Z

src/Algebra/NormalSubgroup.agda

+abelian⇒subgroup-normal : ∀ {c′ ℓ′} → Commutative G._≈_ G._∙_ → (subgroup : Subgroup c′ ℓ′) → IsNormal subgroup
+abelian⇒subgroup-normal ∙-comm subgroup = record { normal = λ n g → ∙-comm (ι n) g }
+  where open Subgroup subgroup


I'd maybe be tempted to lift this out to Algebra.Construct.Quotient.AbelianGroup to bundle up the quotient-out-of-any-subgroup construction, and simplify the downstream imports in #2855 ?

jamesmckinna · 2025-11-05T06:44:25Z

CHANGELOG.md

 New modules
 -----------

+* `Algebra.Cosntruct.Quotient.Group` for the definition of quotient groups.


Typo

Suggested change

* `Algebra.Cosntruct.Quotient.Group` for the definition of quotient groups.

* `Algebra.Construct.Quotient.Group` for the definition of quotient groups.

jamesmckinna · 2025-11-05T06:58:50Z

src/Algebra/Construct/Quotient/Group.agda

+project-isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project
+project-isHomomorphism = record


Naming?

Suggested change

project-isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project

project-isHomomorphism = record

project-isGroupHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project

project-isGroupHomomorphism = record

Twofold reasons:

Subsequently, for Ring R / Ideal I, you also define project-isHomomorphism : IsRingHomomorphism, and maybe that's enough (let the X path context of the algebra determine what kind of IsXHomomorphism is defined

BUT, for Ring, what you actually need is to separate out the isMonoidHomomorphism field, so why not also isGroupHomomorphism?

jamesmckinna · 2025-11-05T07:01:43Z

src/Algebra/Construct/Quotient/Group.agda

+  { isMonoidHomomorphism = record
+    { isMagmaHomomorphism = record
+      { isRelHomomorphism = record
+        { cong = ≈⇒≋
+        }
+      ; homo = λ _ _ → ≋-refl
+      }
+    ; ε-homo = ≋-refl
+    }


This should be lifted out as a separate (prior) definition

project-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma (Group.rawMagma quotientGroup) project project-isMagmaHomomorphism = record { isRelHomomorphism = record { cong = ≈⇒≋ } ; homo = λ _ _ → ≋-refl } project-isMonoidHomomorphism : IsMonoidHomomorphism rawMonoid (Group.rawMonoid quotientGroup) project project-isMonoidHomomorphism = record { isMagmaHomomorphism = project-isMagmaHomomorphism ; ε-homo = ≋-refl } project-isGroupHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project project-isGroupHomomorphism = record { isMonoidHomomorphism = project-isMonoidHomomorphism ; ⁻¹-homo = λ _ → ≋-refl }

jamesmckinna · 2025-11-05T07:28:46Z

src/Algebra/NormalSubgroup.agda

+
+module Algebra.NormalSubgroup {c ℓ} (G : Group c ℓ)  where
+
+open import Algebra.Definitions


jamesmckinna · 2025-11-05T07:40:46Z

src/Algebra/Construct/Quotient/Group.agda

+≈⇒≋ : _≈_ ⇒ _≋_
+≈⇒≋ {x} {y} x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ y)
+


Suggested change

≈⇒≋ : _≈_ ⇒ _≋_

≈⇒≋ {x} {y} x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ y)

In view of the above refactoring of reflexivity...

jamesmckinna · 2025-11-05T07:41:50Z

src/Algebra/Construct/Quotient/Group.agda

+≋-refl : Reflexive _≋_
+≋-refl {x} = N.ε by trans (∙-congʳ ι.ε-homo) (identityˡ x)


Suggested change

≋-refl : Reflexive _≋_

≋-refl {x} = N.ε by trans (∙-congʳ ι.ε-homo) (identityˡ x)

≈⇒≋ : _≈_ ⇒ _≋_

≈⇒≋ {x} {y} x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ y)

≋-refl : Reflexive _≋_

≋-refl = ≈⇒≋ refl

Unsurprisingly, these proofs are definitionally equal to the previous versions, but put ≈⇒≋ ('abstract' reflexivity...) higher up the food chain.

jamesmckinna · 2025-11-05T08:42:58Z

src/Algebra/Construct/Quotient/Group.agda

+open import Algebra.Morphism.Structures using (IsGroupHomomorphism)
+open import Algebra.Properties.Monoid monoid
+open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙)
+open import Algebra.Structures using (IsGroup)


Do we need this import? Cf. #2391 and see below.

jamesmckinna · 2025-11-05T08:46:23Z

src/Algebra/Construct/Quotient/Group.agda

+  }
+
+quotientGroup : Group c (c ⊔ ℓ ⊔ c′)
+quotientGroup = record { isGroup = quotientIsGroup }


And now inline the definition above?

Suggested change

quotientGroup = record { isGroup = quotientIsGroup }

quotientGroup = record

{ isGroup = ...

}

jamesmckinna · 2025-11-06T07:11:23Z

In lieu of any further review comments, please see #2859 (purely!) as a comparison point, and feel free to grab anything from there which you might find useful... it just seemed the easiest way to encapsulate all the thoughts I had had about your groups-rings-modules development

Taneb marked this pull request as draft October 31, 2025 06:42

jamesmckinna approved these changes Oct 31, 2025

View reviewed changes

Taneb force-pushed the quotient-groups branch from 8d0576a to 65c4224 Compare October 31, 2025 09:00

Taneb force-pushed the subgroups branch from 908d364 to 99c90ae Compare October 31, 2025 09:01

Taneb added 3 commits October 31, 2025 10:02

Add normal subgroups and quotient groups

969f670

Factor out Normal, show abelian implies subgroup is normal

69be655

Use symmetric form of normality

e3baf59

I noted that every time I used normal it was under sym This felt like a good reason to reverse it

Taneb force-pushed the quotient-groups branch from 65c4224 to e3baf59 Compare October 31, 2025 09:02

jamesmckinna reviewed Oct 31, 2025

View reviewed changes

src/Algebra/Construct/Quotient/Group.agda Show resolved Hide resolved

jamesmckinna reviewed Oct 31, 2025

View reviewed changes

src/Algebra/NormalSubgroup.agda Outdated Show resolved Hide resolved

Taneb mentioned this pull request Oct 31, 2025

Add ideals and quotient rings #2855

Draft

jamesmckinna reviewed Nov 1, 2025

View reviewed changes

src/Algebra/NormalSubgroup.agda Outdated Show resolved Hide resolved

jamesmckinna reviewed Nov 1, 2025

View reviewed changes

src/Algebra/Construct/Quotient/Group.agda Show resolved Hide resolved

Make Normal a record called IsNormal

60616c1

Taneb commented Nov 3, 2025

View reviewed changes

src/Algebra/NormalSubgroup.agda Outdated Show resolved Hide resolved

Taneb added 3 commits November 3, 2025 10:14

Add _/_ synomym for quotient group

c87e4bf

Remove old Normal definition

40bb8c6

Split product up into two fields in IsNormal

2460cf0

jamesmckinna reviewed Nov 4, 2025

View reviewed changes

jamesmckinna mentioned this pull request Nov 4, 2025

Add subgroups and submodules #2852

Open

jamesmckinna reviewed Nov 5, 2025

View reviewed changes

jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this pull request Nov 5, 2025

refactor: alternative to agda#2852 and agda#2854

d4e36cd

jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this pull request Nov 5, 2025

refactor: alternative to agda#2852 and agda#2854

e2ff677

jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this pull request Nov 5, 2025

refactor: alternative to agda#2852 and agda#2854

f702f82

This was referenced Nov 5, 2025

[ draft ] Alternative design for sub- and quotient- (Abelian)Groups #2859

Draft

[ question/bug ] are infix names allowed for parametrised modules? agda/agda#8191

Open

	* `Algebra.Cosntruct.Quotient.Group` for the definition of quotient groups.
	* `Algebra.Construct.Quotient.Group` for the definition of quotient groups.

		project-isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project
		project-isHomomorphism = record


		module Algebra.NormalSubgroup {c ℓ} (G : Group c ℓ) where

		open import Algebra.Definitions

		≈⇒≋ : _≈_ ⇒ _≋_
		≈⇒≋ {x} {y} x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ y)

		≋-refl : Reflexive _≋_
		≋-refl {x} = N.ε by trans (∙-congʳ ι.ε-homo) (identityˡ x)

Normal subgroups and quotient groups #2854

Are you sure you want to change the base?

Normal subgroups and quotient groups #2854

Uh oh!

Conversation

Taneb commented Oct 31, 2025

Uh oh!

jamesmckinna left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna commented Nov 6, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

jamesmckinna commented Nov 6, 2025 •

edited

Loading